COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro[1,mps]
C00019 ENDMK
C⊗;
\input macro[1,mps]
\input macrwf[1,mps]
\magnification\magstephalf
\baselineskip 14pt
\leftline{\sevenrm A87.Tex[254,rwf]\today}
\leftline{\copyright\sevenrm Robert W. Floyd, September 7, 1989}
\leftline{\sevenrm Unpublished draft}
\bigskip
Let $\langle x↓1, x↓2\rangle$ be the ordered pair with first element $x↓1$ and
second element $x↓2$.  Correspondingly, there are two {\it projection}
functions $h$ and $t$ (head and tail) for which $\langle x↓1, x↓2\rangle 
h = x↓1$ and $\langle x↓1, x↓2\rangle t = x↓2$.

{\narrower\smallskip\noindent
{\bf Drill:} Show if $\langle x↓1, x↓2\rangle = \langle y↓1, y↓2\rangle$, then
$x↓1 = y↓1$ and $x↓2 = y↓2$.\smallskip}

Let {\tt NIL} be a value not in the range of the pairing function $\langle x↓1$,
$x↓2\rangle$, nor in the domain of the projection functions $p↓1$ and $p↓2$.
Using the pairing function and {\tt NIL}, we can define {\it lists} of
arbitrary length.  Inductively, the list of length 0 is $[\,] = {\tt NIL}$.

The list of length $n$, $[x↓1, x↓2, \ldots, x↓n](n\geq 1)$ is defined in terms
of a list of length $n-1$ by
$$[x↓1, x↓2,\ldots, x↓n] = \langle x↓1, [x↓2, x↓3,\ldots, x↓n]\rangle.$$
Specifically,

$$\eqalign{[\,] & = {\tt NIL}\cr
[x↓1] &= \langle x↓1, [\,]\rangle = \langle x↓1, {\tt NIL}\rangle\cr
[x↓1,x↓2] &=\langle x↓1, [x↓2]\rangle = \langle x↓1, \langle x↓2, 
{\tt NIL}\rangle\rangle\cr
[x↓1,x↓2,x↓3] &=\langle x↓1, [x↓2,x↓3]\rangle =\langle x↓1, \langle x↓2,
\langle x↓3, {\tt NIL}\rangle\rangle\rangle\cr
[x↓1,\ldots, x↓n] h &= x↓1\cr
[x↓1,\ldots, x↓n] t &= [x↓2,\ldots, x↓n].\cr}$$

To get the $i↑{th}$ element of the list $[x↓1, x↓2,\ldots, x↓n]$, apply
$t$ to it $i-1$ times, yielding $[x↓i, x↓{i+1},\ldots, x↓n]$; then
apply $h$, yielding $x↓i$.

To determine the {\it length} $n$ of $[x↓1,\ldots, x↓n]$, count how
many times $t$ must be applied to yield {\tt NIL}.

Somestimes we work with an abstract pairing function, about which we need
know only that
$$\eqalign{\langle x, y\rangle h &= x\cr
\langle x, y\rangle t &= y\cr
\langle x, y\rangle &\not= {\tt NIL}.\cr}$$
Sometimes, though, we need a pairing function that can be computed.  A useful
pairing function over $N$ uses {\tt NIL} = 0, $\langle x, y\rangle = 
2↑x(2y+1)$.  The 
projection functions are easily computed: $h(z)$ is the largest number $x$
for which $2↑x$ divides $z$, and $t(z) = (z/2↑{h(z)} - 1)/2$.  When not 
otherwise specified, we use this pairing function over the integers.

{\narrower\smallskip\noindent
{\bf Drill:} Show that, using the above pairing function, the list 
$[x↓1, x↓2, \ldots, x↓n]$ is a number that, expressed in binary, looks like
$10↑{x↓n} 10↑{x↓{n-1}} 1\ldots 10↑{x↓1}.$\smallskip}

A traditional pairing function over $N$ is computed by filling in a table by
diagonals:
\vskip 1.5in
Noticing that $\langle 0,y\rangle = {(2y+3)↑2 -1\over 8}$, we find that
$\langle x,y\rangle = {(2x + 2y + 3)↑2 -1\over 8} - x$.  If $z = \langle x,y
\rangle$, we find $x+y = \lceil{\sqrt{8z+1} - 3\over 2}\rceil$, $x = 8z+1 - 
(2(x+y)+3)↑2$, $y = (x+y) - x$.  For practical purposes, $2↑x(2y+1)$ 
is more useful.

Another traditional pairing function is $\langle x,y\rangle = 2↑x3↑y$.  This
function was used extensively by Kurt G\"odel {\rm (``Gerdl'')},
and lists expressed using pairing functions, especially this one, are called
G\"odel numbers.

If a machine consists of devices $D↓1, D↓2,\ldots, D↓n$, and device $D↓i$
is in state $S↓i$, we can describe all the states by the single list
$[S↓1, S↓2,\ldots, S↓n]$, called a {\it configuration} of the
machine.  Naturally, we must specify a particular sequence of the devices.
When not explicitly specified, we will use the order control, input,
storage, output.

If $\rho↓1$ and $\rho↓2$ are relations, we define a paired relation
$\langle\!\langle\rho↓1, \rho↓2\rangle\!\rangle$ between ordered pairs by
$$\langle x↓1, x↓2\rangle \langle\!\langle\rho↓1, \rho↓2\rangle\!\rangle\langle
y↓1, y↓2\rangle \equiv x↓1\rho↓1y↓1 \land x↓2\rho↓2y↓2.$$
For example,
$$\langle{\rm Joe, Ali}\rangle\langle\!\langle{\rm uncle, son}\rangle\!\rangle
\langle{\rm Sarah, Ruzena}\rangle$$
when Joe is Sarah's uncle, and Ali is Ruzena's son.  We can extend this idea to 
lists of relations by defining a list relation $\lbrack\!\lbrack\rho↓1,\rho↓2,
\ldots,\rho↓n\rbrack\!\rbrack$ for which $[x↓1,\ldots, x↓n]\lbrack\!\lbrack
\rho↓1,\ldots,\rho↓n\rbrack\!\rbrack\lbrack y↓1,\ldots, y↓n]$ when
$x↓1\rho↓1y↓1$, $x↓2\rho↓2y↓2$,$\dots,x↓n\rho↓ny↓n$.  The list relations can
be defined in terms of paired relations:
$$\lbrack\!\lbrack\rho↓1,\ldots,\rho↓n\rbrack\!\rbrack = \langle\!\langle
\rho↓1,\lbrack\!\lbrack\rho↓2,\ldots,\rho↓n\rbrack\!\rbrack\rangle\!\rangle$$
$$\lbrack\!\lbrack\,\rbrack\!\rbrack{\rm is} \{\langle {\tt NIL}, 
{\tt NIL}\rangle\}.$$
For example,
$$\eqalign {&[x↓1, x↓2]\lbrack\!\lbrack\rho↓1,\rho↓2\rbrack\!\rbrack [y↓1, y↓2]\cr
&\qquad = \langle x↓1, [x↓2]\rangle\langle\!\langle\rho↓1, \lbrack\!\lbrack
\rho↓2\rbrack\!\rbrack\rangle\!\rangle\langle y↓1, [y↓2]\rangle\cr
&\qquad = x↓1\rho↓1y↓1\land [x↓2]\lbrack\!\lbrack\rho↓2\rbrack\!\rbrack [y↓2]\cr
&\qquad = x↓1\rho↓1y↓1\land\langle x↓2,{\tt NIL}\rangle\langle\!\langle\rho↓2,
\lbrack\!\lbrack\,\rbrack\!\rbrack\rangle\!\rangle\langle y↓2, {\tt NIL}
\rangle\cr
&\qquad = x↓1\rho↓1y↓1\land x↓2\rho↓2y↓2\land{\tt NIL}\lbrack\!\lbrack
\,\rbrack\!\rbrack{\tt NIL}\cr
&\qquad = x↓1\rho↓1y↓1\land x↓2\rho↓2y↓2.\cr}$$
As we defined configurations of a machine as lists of states, one for each
device, we define instructions of a program for that machine as lists of
operations, one for each device.  If the machine is
$${\tt control, input, Rstack, Lstack, output,}$$
then the relation
$$[3, aw, xd, y, z]\lbrack\!\lbrack 3\rightarrow 5, {\rm scan}\, a,
{\rm pop}\, d, {\rm push}\, d, {\rm write}\, e 
\rbrack\!\rbrack [5,w,x,dy,ze]$$
shows one possible step of the machine.

Using pairing functions, we can construct from any two devices a single device 
that can replace them.  If $D↓1$ and $D↓2$ are the devices, let $\langle D↓1, 
D↓2\rangle$ be the paired device.  Its states are $\langle S↓1, S↓2\rangle$
where $S↓i$ is a state of $D↓i$.  Its operations are $\langle\!\langle
\rho↓1, \rho↓2\rangle\!\rangle$, where $\rho↓i$ is an operation of $D↓i$.
If we combine the first two devices of machine $M$, we get $M'$ with devices
$\langle D↓1, D↓2\rangle, D↓3,\ldots, D↓n$.  Its initializer maps argument
$x$ into $[\langle x\alpha↓1, x\alpha↓2\rangle, x\alpha↓3, \ldots, x\alpha↓n]$.
If a computation of $M$ uses the step
$$[u↓1, u↓2, u↓3,\ldots, u↓n]\lbrack\!\lbrack\rho↓1, \rho↓2, \rho↓3,\ldots,
\rho↓n\rbrack\!\rbrack [v↓1, \ldots, u↓n]$$
the corresponding computation of $M↑1$ uses
$$[\langle u↓1, u↓2\rangle, u↓3,\ldots, u↓n]\lbrack\!\lbrack\rangle\!\rangle
\rho↓1, \rho↓2\rangle\!\rangle, \rho↓3,\ldots, \rho↓n\rbrack\!\rbrack [\langle
v↓1, v↓2,\rangle,\ldots, v↓n].$$
So, if we want to pay attention in a proof to only a few devices of a machine,
we may combine all the others into a single device.  If a machine has two controls,
they can be paired into a single control, because
$$\langle\!\langle i\rightarrow j, k\rightarrow l\rangle\!\rangle = \langle i,k
\rangle \rightarrow\langle j, l\rangle.$$
In addition to pairing devices, we may list devices, using the convention
that the empty list of devices is a device with a single state, 
{\tt NIL}, and a single operation, {\tt NIL} $\rightarrow$ {\tt NIL}.

Next we show how a machine $M'$ with input repertory $\{{\rm scan}\, a,$
${\rm scan} \, b$,
${\rm eof}\}$ can simulate a machine $M$ with input repertory also including
next$\,a$, next$\,b$.  Combine all other devices of $M$ into a single device.

The devices of $M$ are [input, other] and those of $M↑\prime$ are [buffer, input,
other] where buffer is a control with states $\{\Lambda,a,b,e\}$.  The
representation is $\rho = \rho↓\Lambda\cup\rho↓a\cup\rho↓b\cup\rho↓e$, where
$$\displaylines{[\Lambda,u,v]\rho↓\Lambda [u,v]\cr
[a,u,v]\rho↓a [au,v]\cr
[b,u,v]\rho↓b [bu,v]\cr
[e,\Lambda,v]\rho↓e [\Lambda,v].\cr}$$
The instructions of $P↑\prime$ always include
$$\displaylines{[\Lambda\rightarrow a, {\rm scan}\, a, \delta]\cr
[\Lambda\rightarrow b, {\rm scan}\, b, \delta]\cr
[\Lambda\rightarrow e, {\rm eof}, \delta]\cr}$$
Additionally, if the instruction in the left column is in $P$ below, the
instruction in the right column is in $P↑\prime$:
$$\vbox{\halign{$#$\hfill &\qquad $#$ \hfill\cr
[{\rm scan}\, a, \rho] & [a\rightarrow\Lambda,\delta,\rho]\cr
[{\rm scan}\, b, \rho] & [b\rightarrow\Lambda,\delta,\rho]\cr
[{\rm eof}\, \rho] & [e\rightarrow e,\delta,\rho]\cr
[{\rm next}\, a,\rho] & [a\rightarrow a,\delta,\rho]\cr
[{\rm next}\, b,\rho] & [b\rightarrow b,\delta,\rho]\cr
[\delta,\rho] & [\delta,\delta,\rho]\cr}}$$
If the initializer of $M$ is $[\alpha↓{\rm input}$, $\alpha↓{\rm other}]$,
then that of $M↑\prime$ is $[X\times\Lambda$, $\alpha↓{\rm input}$,
$\alpha↓{\rm other}]$.  If the finalizer of $M$ is $[\Lambda\times Y$, 
$\omega↓{\rm other}]$, then that of $M↑\prime$ is $[e\times Y$, 
$\Lambda\times Y$, $\omega↓{\rm other}]$.

Then the diagrams below commute:  [RWF:  draft illustrations]
\vfill\eject
Notice that the instructions in $P↑\prime$ that execute eof also change the
buffer to $e$.  When the buffer becomes $e$, it never changes again.  When
the buffer is $e$, no input operation is performed.

Input operations in $P'$ are not performed by the same instructions as other
operations.  The input operations of a computation of $P'$ must consist of enough
scans to consume the input, followed by one eof.  Since the input file
is initially finite, no computation of $P↑\prime$ can perform infinitely
many input operations.

The control operations of $P↑\prime$ can of course be combined with the buffer
operations, without changing the above properties.

{\narrower\smallskip\noindent
{\bf Drill:}  Show that $P$ simulates $P↑\prime$.\smallskip}
\bye